Inference at * 1 2 0 
Iof proof for Lemma decidable and:



1. P : 
2. Q : 
3. P
4. Q
  (P  Q)  ((P  Q)) 

latex

 by PERMUTE{1:n, 2:n, 2:n} 

latex

 1: 

 1: 5. P  Q
 1:   False
 2: .....wf..... NILNIL

 2:   (P  Q)  
 .

Definitions

t  T, Type, s = t, x:AB(x), False, left + right, P  Q, , P  Q, P  Q, A